00100	
00200	
00300	(DEFPROP FINI 
00400	 (LAMBDA(U R Z1 Z2 E)
00500	  (PROG (Z)
00600		(COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
00700		(COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
00800		(SETQ COUNT (PLUS COUNT (LENGTH R)))
00900		(SETQ R (EDIT U R))
01000		(CLAUSES2 R)
01100		(COND ((NULL R) (RETURN 0)))
01200		(BAKSUB CLAUSES R)
01300		(BOOKEEP E R (CONS Z1 Z2))
01400		(SETQ Z (UNITPN R))
01500		(SETQ UNAXP (APPEND (CAR Z) UNAXP))
01600		(SETQ UNAXN (APPEND (CDR Z) UNAXN))
01700	(COND((NOT PFLG)(COND(DLIST(NCONC DLIST(EQUNITS(CAR Z))))
01710					(T(SETQ DLIST(EQUNITS UNAXP))))))
01800		(RETURN (LENGTH R)))) 
01900	EXPR)
02000	
02100	(DE EQUNITS(X)
02200	(PROG (Z)
02300	A(COND((NULL X)(RETURN Z))
02400	((EQ EQUAL (CAADAR X))(SETQ Z (CONS (CAR X) Z))) )
02500	(SETQ X(CDR X))
02600	(GO A) ))